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