Bob is not quiet. Bob is rough. Bob is round. Bob is young. Charlie is green. Charlie is nice. Charlie is rough. Charlie is young. Gary is cold. Gary is green. Harry is nice. Harry is rough. All quiet, cold things are not green. If something is young and not quiet then it is not green. Rough things are young. Nice, cold things are young. If Harry is nice then Harry is young. All cold, green things are nice. All young, quiet things are cold. If Bob is quiet then Bob is green.
Bob is not quiet.
("Bob" "is" "quiet" "-")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is young.
("Bob" "is" "young" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is green.
("Gary" "is" "green" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is rough.
("Harry" "is" "rough" "+")
All quiet, cold things are not green.
((("something" "is" "quiet" "+") ("something" "is" "cold" "+")) -> ("something" "is" "green" "-"))
If something is young and not quiet then it is not green.
((("something" "is" "young" "+") ("something" "is" "quiet" "~")) -> ("something" "is" "green" "-"))
Rough things are young.
((("something" "is" "rough" "+")) -> ("something" "is" "young" "+"))
Nice, cold things are young.
((("something" "is" "nice" "+") ("something" "is" "cold" "+")) -> ("something" "is" "young" "+"))
If Harry is nice then Harry is young.
((("Harry" "is" "nice" "+")) -> ("Harry" "is" "young" "+"))
All cold, green things are nice.
((("something" "is" "cold" "+") ("something" "is" "green" "+")) -> ("something" "is" "nice" "+"))
All young, quiet things are cold.
((("something" "is" "young" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "cold" "+"))
If Bob is quiet then Bob is green.
((("Bob" "is" "quiet" "+")) -> ("Bob" "is" "green" "+"))
Charlie is green.
True
1
proof
[(triple5)]
("Charlie" "is" "green" "+")
triple5
Bob is not round.
False
1
inv-proof
[(triple3)]
("Bob" "is" "round" "-")
triple3
Harry is young.
True
2
proof
[(((triple11) -> rule5) OR ((triple12) -> rule3))]
("Harry" "is" "young" "+")
((triple11) -> (rule5 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
((triple12) -> (rule3 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is not young.
False
2
inv-proof
[(((triple11) -> rule5) OR ((triple12) -> rule3))]
("Harry" "is" "young" "-")
((triple11) -> (rule5 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
((triple12) -> (rule3 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Gary is young.
True
5
proof
[(((((triple9 triple10) -> rule6) triple9) -> rule4))]
("Gary" "is" "young" "+")
((((triple9 triple10) -> (rule6 % int2)) triple9) -> (rule4 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is not young.
False
5
inv-proof
[(((((triple9 triple10) -> rule6) triple9) -> rule4))]
("Gary" "is" "young" "-")
((((triple9 triple10) -> (rule6 % int2)) triple9) -> (rule4 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Bob is not nice.
Unknown
inv-rconc
[@1: Bob is nice.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Bob" "is" "nice" "-")
Charlie is cold.
Unknown
rconc
[@1: Charlie is cold.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Charlie" "is" "cold" "+")
Harry is not cold.
Unknown
inv-rconc
[@1: Harry is cold.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Harry" "is" "cold" "-")
Charlie is round.
Unknown
random
[@0: Charlie is round.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "round" "+")
Gary is not quiet.
Unknown
inv-random
[@0: Gary is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "quiet" "-")
Harry is quiet.
Unknown
random
[@0: Harry is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "quiet" "+")
@0: Bob is not quiet.[(triple1)] Bob is rough.[(triple2)] Bob is round.[(triple3)] Bob is young.[(triple4 OR ((triple2) -> rule3))] Charlie is green.[(triple5)] Charlie is nice.[(triple6)] Charlie is rough.[(triple7)] Charlie is young.[(triple8 OR ((triple7) -> rule3))] Gary is cold.[(triple9)] Gary is green.[(triple10)] Harry is nice.[(triple11)] Harry is rough.[(triple12)] @1: Bob is not green.[(((triple4 triple1) -> rule2) OR ((((triple2) -> rule3) triple1) -> rule2))] Gary is nice.[(((triple9 triple10) -> rule6))] Harry is young.[(((triple11) -> rule5) OR ((triple12) -> rule3))] @2: Gary is young.[(((((triple9 triple10) -> rule6) triple9) -> rule4))]
Bob is not quiet.
("Bob" "is" "quiet" "-")
triple1
Bob is rough.
("Bob" "is" "rough" "+")
triple2
Bob is round.
("Bob" "is" "round" "+")
triple3
Bob is young.
("Bob" "is" "young" "+")
triple4
((triple2) -> (rule3 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
triple5
Charlie is nice.
("Charlie" "is" "nice" "+")
triple6
Charlie is rough.
("Charlie" "is" "rough" "+")
triple7
Charlie is young.
("Charlie" "is" "young" "+")
triple8
((triple7) -> (rule3 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
triple9
Gary is green.
("Gary" "is" "green" "+")
triple10
Harry is nice.
("Harry" "is" "nice" "+")
triple11
Harry is rough.
("Harry" "is" "rough" "+")
triple12
Bob is not green.
("Bob" "is" "green" "-")
((triple4 triple1) -> (rule2 % int1))
Bob is not green.
("Bob" "is" "green" "-")
int1
((((triple2) -> (rule3 % int2)) triple1) -> (rule2 % int1))
Bob is not green.
("Bob" "is" "green" "-")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
((triple9 triple10) -> (rule6 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
((triple11) -> (rule5 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
((triple12) -> (rule3 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
((((triple9 triple10) -> (rule6 % int2)) triple9) -> (rule4 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2