Bob is cold. Charlie is cold. Charlie is kind. Charlie is young. Fiona is rough. Fiona is young. Harry is cold. Harry is green. Harry is kind. Harry is red. Harry is rough. Harry is round. All kind people are rough. If someone is kind then they are rough.
Bob is cold.
("Bob" "is" "cold" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Fiona is young.
("Fiona" "is" "young" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is round.
("Harry" "is" "round" "+")
All kind people are rough.
((("someone" "is" "kind" "+")) -> ("someone" "is" "rough" "+"))
If someone is kind then they are rough.
((("someone" "is" "kind" "+")) -> ("someone" "is" "rough" "+"))
Charlie is kind.
True
1
proof
[(triple3)]
("Charlie" "is" "kind" "+")
triple3
Charlie is not young.
False
1
inv-proof
[(triple4)]
("Charlie" "is" "young" "-")
triple4
Charlie is rough.
True
2
proof
[(((triple3) -> rule1) OR ((triple3) -> rule2))]
("Charlie" "is" "rough" "+")
((triple3) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
((triple3) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is not rough.
False
2
inv-proof
[(((triple3) -> rule1) OR ((triple3) -> rule2))]
("Charlie" "is" "rough" "-")
((triple3) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
((triple3) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Bob is not rough.
Unknown
inv-rconc
[@1: Bob is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "rough" "-")
Fiona is round.
Unknown
random
[@0: Fiona is round.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "round" "+")
Fiona is not red.
Unknown
inv-random
[@0: Fiona is red.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "red" "-")
Charlie is red.
Unknown
random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "+")
@0: Bob is cold.[(triple1)] Charlie is cold.[(triple2)] Charlie is kind.[(triple3)] Charlie is young.[(triple4)] Fiona is rough.[(triple5)] Fiona is young.[(triple6)] Harry is cold.[(triple7)] Harry is green.[(triple8)] Harry is kind.[(triple9)] Harry is red.[(triple10)] Harry is rough.[(triple11 OR ((triple9) -> rule1) OR ((triple9) -> rule2))] Harry is round.[(triple12)] @1: Charlie is rough.[(((triple3) -> rule1) OR ((triple3) -> rule2))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
Charlie is cold.
("Charlie" "is" "cold" "+")
triple2
Charlie is kind.
("Charlie" "is" "kind" "+")
triple3
Charlie is young.
("Charlie" "is" "young" "+")
triple4
Fiona is rough.
("Fiona" "is" "rough" "+")
triple5
Fiona is young.
("Fiona" "is" "young" "+")
triple6
Harry is cold.
("Harry" "is" "cold" "+")
triple7
Harry is green.
("Harry" "is" "green" "+")
triple8
Harry is kind.
("Harry" "is" "kind" "+")
triple9
Harry is red.
("Harry" "is" "red" "+")
triple10
Harry is rough.
("Harry" "is" "rough" "+")
triple11
((triple9) -> (rule1 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
((triple9) -> (rule2 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
triple12
Charlie is rough.
("Charlie" "is" "rough" "+")
((triple3) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
((triple3) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1