Bob is blue. Bob is green. Bob is kind. Bob is rough. Charlie is blue. Charlie is cold. Charlie is green. Charlie is kind. Charlie is rough. Charlie is smart. Gary is cold. Harry is blue. Harry is kind. Harry is rough. Harry is smart. All rough, green things are young. If something is kind then it is rough. All young things are rough. Cold things are young. If Bob is green then Bob is smart. If Bob is young and Bob is kind then Bob is smart. All cold, kind things are rough. If Charlie is rough and Charlie is smart then Charlie is kind.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is smart.
("Harry" "is" "smart" "+")
All rough, green things are young.
((("something" "is" "rough" "+") ("something" "is" "green" "+")) -> ("something" "is" "young" "+"))
If something is kind then it is rough.
((("something" "is" "kind" "+")) -> ("something" "is" "rough" "+"))
All young things are rough.
((("something" "is" "young" "+")) -> ("something" "is" "rough" "+"))
Cold things are young.
((("something" "is" "cold" "+")) -> ("something" "is" "young" "+"))
If Bob is green then Bob is smart.
((("Bob" "is" "green" "+")) -> ("Bob" "is" "smart" "+"))
If Bob is young and Bob is kind then Bob is smart.
((("Bob" "is" "young" "+") ("Bob" "is" "kind" "+")) -> ("Bob" "is" "smart" "+"))
All cold, kind things are rough.
((("something" "is" "cold" "+") ("something" "is" "kind" "+")) -> ("something" "is" "rough" "+"))
If Charlie is rough and Charlie is smart then Charlie is kind.
((("Charlie" "is" "rough" "+") ("Charlie" "is" "smart" "+")) -> ("Charlie" "is" "kind" "+"))
Harry is rough.
True
1
proof
[(triple14 OR ((triple13) -> rule2))]
("Harry" "is" "rough" "+")
triple14
((triple13) -> (rule2 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Charlie is not smart.
False
1
inv-proof
[(triple10)]
("Charlie" "is" "smart" "-")
triple10
Gary is young.
True
2
proof
[(((triple11) -> rule4))]
("Gary" "is" "young" "+")
((triple11) -> (rule4 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Charlie is not young.
False
2
inv-proof
[(((triple6) -> rule4) OR ((triple9 triple7) -> rule1) OR ((((triple8) -> rule2) triple7) -> rule1) OR ((((triple6 triple8) -> rule7) triple7) -> rule1))]
("Charlie" "is" "young" "-")
((triple6) -> (rule4 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
((triple9 triple7) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
((((triple8) -> (rule2 % int2)) triple7) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
((((triple6 triple8) -> (rule7 % int2)) triple7) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Gary is rough.
True
3
proof
[(((((triple11) -> rule4)) -> rule3))]
("Gary" "is" "rough" "+")
((((triple11) -> (rule4 % int2))) -> (rule3 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is not rough.
False
3
inv-proof
[(((((triple11) -> rule4)) -> rule3))]
("Gary" "is" "rough" "-")
((((triple11) -> (rule4 % int2))) -> (rule3 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Harry is not young.
Unknown
inv-rconc
[@1: Harry is young.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "young" "-")
Gary is blue.
Unknown
random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "+")
Gary is not green.
Unknown
inv-random
[@0: Gary is green.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "green" "-")
Harry is green.
Unknown
random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "+")
Gary is not smart.
Unknown
inv-random
[@0: Gary is smart.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "smart" "-")
Bob is cold.
Unknown
random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "+")
@0: Bob is blue.[(triple1)] Bob is green.[(triple2)] Bob is kind.[(triple3)] Bob is rough.[(triple4 OR ((triple3) -> rule2))] Charlie is blue.[(triple5)] Charlie is cold.[(triple6)] Charlie is green.[(triple7)] Charlie is kind.[(triple8 OR ((triple9 triple10) -> rule8) OR ((((((triple6) -> rule4)) -> rule3) triple10) -> rule8))] Charlie is rough.[(triple9 OR ((triple8) -> rule2) OR ((triple6 triple8) -> rule7) OR ((((triple6) -> rule4)) -> rule3))] Charlie is smart.[(triple10)] Gary is cold.[(triple11)] Harry is blue.[(triple12)] Harry is kind.[(triple13)] Harry is rough.[(triple14 OR ((triple13) -> rule2))] Harry is smart.[(triple15)] @1: Bob is smart.[(((triple2) -> rule5) OR ((((triple4 triple2) -> rule1) triple3) -> rule6) OR ((((((triple3) -> rule2) triple2) -> rule1) triple3) -> rule6))] Bob is young.[(((triple4 triple2) -> rule1) OR ((((triple3) -> rule2) triple2) -> rule1))] Charlie is young.[(((triple6) -> rule4) OR ((triple9 triple7) -> rule1) OR ((((triple8) -> rule2) triple7) -> rule1) OR ((((triple6 triple8) -> rule7) triple7) -> rule1))] Gary is young.[(((triple11) -> rule4))] @2: Gary is rough.[(((((triple11) -> rule4)) -> rule3))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is green.
("Bob" "is" "green" "+")
triple2
Bob is kind.
("Bob" "is" "kind" "+")
triple3
Bob is rough.
("Bob" "is" "rough" "+")
triple4
((triple3) -> (rule2 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
triple5
Charlie is cold.
("Charlie" "is" "cold" "+")
triple6
Charlie is green.
("Charlie" "is" "green" "+")
triple7
Charlie is kind.
("Charlie" "is" "kind" "+")
triple8
((triple9 triple10) -> (rule8 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
((((((triple6) -> (rule4 % int3))) -> (rule3 % int2)) triple10) -> (rule8 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3
Charlie is rough.
("Charlie" "is" "rough" "+")
triple9
((triple8) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
((triple6 triple8) -> (rule7 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
((((triple6) -> (rule4 % int2))) -> (rule3 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
triple10
Gary is cold.
("Gary" "is" "cold" "+")
triple11
Harry is blue.
("Harry" "is" "blue" "+")
triple12
Harry is kind.
("Harry" "is" "kind" "+")
triple13
Harry is rough.
("Harry" "is" "rough" "+")
triple14
((triple13) -> (rule2 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
triple15
Bob is smart.
("Bob" "is" "smart" "+")
((triple2) -> (rule5 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
((((triple4 triple2) -> (rule1 % int2)) triple3) -> (rule6 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
((((((triple3) -> (rule2 % int3)) triple2) -> (rule1 % int2)) triple3) -> (rule6 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Bob is young.
("Bob" "is" "young" "+")
((triple4 triple2) -> (rule1 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
((((triple3) -> (rule2 % int2)) triple2) -> (rule1 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
((triple6) -> (rule4 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
((triple9 triple7) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
((((triple8) -> (rule2 % int2)) triple7) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
((((triple6 triple8) -> (rule7 % int2)) triple7) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
((triple11) -> (rule4 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
((((triple11) -> (rule4 % int2))) -> (rule3 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2