Charlie is blue. Charlie is not cold. Charlie is green. Charlie is smart. Fiona is big. Fiona is rough. Gary is not big. Gary is blue. Gary is cold. Gary is quiet. Harry is big. Harry is blue. Harry is green. Harry is quiet. Harry is not rough. Harry is smart. All green people are big. If someone is smart then they are green. If someone is smart then they are green. All big, cold people are quiet. If someone is rough and big then they are cold. All smart people are blue. Quiet, cold people are blue. If Gary is big and Gary is quiet then Gary is cold. If Fiona is blue then Fiona is smart.
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is not cold.
("Charlie" "is" "cold" "-")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Gary is not big.
("Gary" "is" "big" "-")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is not rough.
("Harry" "is" "rough" "-")
Harry is smart.
("Harry" "is" "smart" "+")
All green people are big.
((("someone" "is" "green" "+")) -> ("someone" "is" "big" "+"))
If someone is smart then they are green.
((("someone" "is" "smart" "+")) -> ("someone" "is" "green" "+"))
If someone is smart then they are green.
((("someone" "is" "smart" "+")) -> ("someone" "is" "green" "+"))
All big, cold people are quiet.
((("someone" "is" "big" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "quiet" "+"))
If someone is rough and big then they are cold.
((("someone" "is" "rough" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "cold" "+"))
All smart people are blue.
((("someone" "is" "smart" "+")) -> ("someone" "is" "blue" "+"))
Quiet, cold people are blue.
((("someone" "is" "quiet" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "blue" "+"))
If Gary is big and Gary is quiet then Gary is cold.
((("Gary" "is" "big" "+") ("Gary" "is" "quiet" "+")) -> ("Gary" "is" "cold" "+"))
If Fiona is blue then Fiona is smart.
((("Fiona" "is" "blue" "+")) -> ("Fiona" "is" "smart" "+"))
Charlie is blue.
True
1
proof
[(triple1 OR ((triple4) -> rule6))]
("Charlie" "is" "blue" "+")
triple1
((triple4) -> (rule6 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Harry is not blue.
False
1
inv-proof
[(triple12 OR ((triple16) -> rule6))]
("Harry" "is" "blue" "-")
triple12
((triple16) -> (rule6 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Fiona is cold.
True
3
proof
[(((triple6 triple5) -> rule5))]
("Fiona" "is" "cold" "+")
((triple6 triple5) -> (rule5 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Charlie is not big.
False
2
inv-proof
[(((triple3) -> rule1) OR ((((triple4) -> rule2)) -> rule1) OR ((((triple4) -> rule3)) -> rule1))]
("Charlie" "is" "big" "-")
((triple3) -> (rule1 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
((((triple4) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
((((triple4) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Fiona is quiet.
True
5
proof
[(((triple5 ((triple6 triple5) -> rule5)) -> rule4))]
("Fiona" "is" "quiet" "+")
((triple5 ((triple6 triple5) -> (rule5 % int2))) -> (rule4 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is not quiet.
False
5
inv-proof
[(((triple5 ((triple6 triple5) -> rule5)) -> rule4))]
("Fiona" "is" "quiet" "-")
((triple5 ((triple6 triple5) -> (rule5 % int2))) -> (rule4 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is blue.
True
9
proof
[(((((triple5 ((triple6 triple5) -> rule5)) -> rule4) ((triple6 triple5) -> rule5)) -> rule7))]
("Fiona" "is" "blue" "+")
((((triple5 ((triple6 triple5) -> (rule5 % int3))) -> (rule4 % int2)) ((triple6 triple5) -> (rule5 % int3))) -> (rule7 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
int3
Fiona is not blue.
False
9
inv-proof
[(((((triple5 ((triple6 triple5) -> rule5)) -> rule4) ((triple6 triple5) -> rule5)) -> rule7))]
("Fiona" "is" "blue" "-")
((((triple5 ((triple6 triple5) -> (rule5 % int3))) -> (rule4 % int2)) ((triple6 triple5) -> (rule5 % int3))) -> (rule7 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
int3
Fiona is smart.
True
10
proof
[(((((((triple5 ((triple6 triple5) -> rule5)) -> rule4) ((triple6 triple5) -> rule5)) -> rule7)) -> rule9))]
("Fiona" "is" "smart" "+")
((((((triple5 ((triple6 triple5) -> (rule5 % int4))) -> (rule4 % int3)) ((triple6 triple5) -> (rule5 % int4))) -> (rule7 % int2))) -> (rule9 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int3
Fiona is cold.
("Fiona" "is" "cold" "+")
int4
Fiona is not smart.
False
10
inv-proof
[(((((((triple5 ((triple6 triple5) -> rule5)) -> rule4) ((triple6 triple5) -> rule5)) -> rule7)) -> rule9))]
("Fiona" "is" "smart" "-")
((((((triple5 ((triple6 triple5) -> (rule5 % int4))) -> (rule4 % int3)) ((triple6 triple5) -> (rule5 % int4))) -> (rule7 % int2))) -> (rule9 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int3
Fiona is cold.
("Fiona" "is" "cold" "+")
int4
Fiona is green.
True
11
proof
[(((((((((triple5 ((triple6 triple5) -> rule5)) -> rule4) ((triple6 triple5) -> rule5)) -> rule7)) -> rule9)) -> rule2) OR ((((((((triple5 ((triple6 triple5) -> rule5)) -> rule4) ((triple6 triple5) -> rule5)) -> rule7)) -> rule9)) -> rule3))]
("Fiona" "is" "green" "+")
((((((((triple5 ((triple6 triple5) -> (rule5 % int5))) -> (rule4 % int4)) ((triple6 triple5) -> (rule5 % int5))) -> (rule7 % int3))) -> (rule9 % int2))) -> (rule2 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
int3
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int4
Fiona is cold.
("Fiona" "is" "cold" "+")
int5
((((((((triple5 ((triple6 triple5) -> (rule5 % int5))) -> (rule4 % int4)) ((triple6 triple5) -> (rule5 % int5))) -> (rule7 % int3))) -> (rule9 % int2))) -> (rule3 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
int3
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int4
Fiona is cold.
("Fiona" "is" "cold" "+")
int5
Fiona is not green.
False
11
inv-proof
[(((((((((triple5 ((triple6 triple5) -> rule5)) -> rule4) ((triple6 triple5) -> rule5)) -> rule7)) -> rule9)) -> rule2) OR ((((((((triple5 ((triple6 triple5) -> rule5)) -> rule4) ((triple6 triple5) -> rule5)) -> rule7)) -> rule9)) -> rule3))]
("Fiona" "is" "green" "-")
((((((((triple5 ((triple6 triple5) -> (rule5 % int5))) -> (rule4 % int4)) ((triple6 triple5) -> (rule5 % int5))) -> (rule7 % int3))) -> (rule9 % int2))) -> (rule2 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
int3
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int4
Fiona is cold.
("Fiona" "is" "cold" "+")
int5
((((((((triple5 ((triple6 triple5) -> (rule5 % int5))) -> (rule4 % int4)) ((triple6 triple5) -> (rule5 % int5))) -> (rule7 % int3))) -> (rule9 % int2))) -> (rule3 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
int3
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int4
Fiona is cold.
("Fiona" "is" "cold" "+")
int5
Charlie is not quiet.
Unknown
inv-rconc
[@1: Charlie is quiet.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Charlie" "is" "quiet" "-")
Gary is green.
Unknown
rconc
[@1: Gary is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "green" "+")
Harry is not cold.
Unknown
inv-rconc
[@1: Harry is cold.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Harry" "is" "cold" "-")
Charlie is rough.
Unknown
random
[@0: Charlie is rough.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "rough" "+")
Gary is not rough.
Unknown
inv-random
[@0: Gary is rough.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "rough" "-")
Gary is smart.
Unknown
random
[@0: Gary is smart.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "smart" "+")
@0: Charlie is blue.[(triple1 OR ((triple4) -> rule6))] Charlie is green.[(triple3 OR ((triple4) -> rule2) OR ((triple4) -> rule3))] Charlie is not cold.[(triple2)] Charlie is smart.[(triple4)] Fiona is big.[(triple5)] Fiona is rough.[(triple6)] Gary is blue.[(triple8 OR ((triple10 triple9) -> rule7))] Gary is cold.[(triple9)] Gary is not big.[(triple7)] Gary is quiet.[(triple10)] Harry is big.[(triple11 OR ((triple13) -> rule1) OR ((((triple16) -> rule2)) -> rule1) OR ((((triple16) -> rule3)) -> rule1))] Harry is blue.[(triple12 OR ((triple16) -> rule6))] Harry is green.[(triple13 OR ((triple16) -> rule2) OR ((triple16) -> rule3))] Harry is not rough.[(triple15)] Harry is quiet.[(triple14)] Harry is smart.[(triple16)] @1: Charlie is big.[(((triple3) -> rule1) OR ((((triple4) -> rule2)) -> rule1) OR ((((triple4) -> rule3)) -> rule1))] Fiona is cold.[(((triple6 triple5) -> rule5))] @2: Fiona is quiet.[(((triple5 ((triple6 triple5) -> rule5)) -> rule4))] @3: Fiona is blue.[(((((triple5 ((triple6 triple5) -> rule5)) -> rule4) ((triple6 triple5) -> rule5)) -> rule7))] @4: Fiona is smart.[(((((((triple5 ((triple6 triple5) -> rule5)) -> rule4) ((triple6 triple5) -> rule5)) -> rule7)) -> rule9))] @5: Fiona is green.[(((((((((triple5 ((triple6 triple5) -> rule5)) -> rule4) ((triple6 triple5) -> rule5)) -> rule7)) -> rule9)) -> rule2) OR ((((((((triple5 ((triple6 triple5) -> rule5)) -> rule4) ((triple6 triple5) -> rule5)) -> rule7)) -> rule9)) -> rule3))]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
((triple4) -> (rule6 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
triple3
((triple4) -> (rule2 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
((triple4) -> (rule3 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is not cold.
("Charlie" "is" "cold" "-")
triple2
Charlie is smart.
("Charlie" "is" "smart" "+")
triple4
Fiona is big.
("Fiona" "is" "big" "+")
triple5
Fiona is rough.
("Fiona" "is" "rough" "+")
triple6
Gary is blue.
("Gary" "is" "blue" "+")
triple8
((triple10 triple9) -> (rule7 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
triple9
Gary is not big.
("Gary" "is" "big" "-")
triple7
Gary is quiet.
("Gary" "is" "quiet" "+")
triple10
Harry is big.
("Harry" "is" "big" "+")
triple11
((triple13) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
((((triple16) -> (rule2 % int2))) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
((((triple16) -> (rule3 % int2))) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
triple12
((triple16) -> (rule6 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
triple13
((triple16) -> (rule2 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
((triple16) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is not rough.
("Harry" "is" "rough" "-")
triple15
Harry is quiet.
("Harry" "is" "quiet" "+")
triple14
Harry is smart.
("Harry" "is" "smart" "+")
triple16
Charlie is big.
("Charlie" "is" "big" "+")
((triple3) -> (rule1 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
((((triple4) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
((((triple4) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
((triple6 triple5) -> (rule5 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
((triple5 ((triple6 triple5) -> (rule5 % int2))) -> (rule4 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
((((triple5 ((triple6 triple5) -> (rule5 % int3))) -> (rule4 % int2)) ((triple6 triple5) -> (rule5 % int3))) -> (rule7 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
int3
Fiona is smart.
("Fiona" "is" "smart" "+")
((((((triple5 ((triple6 triple5) -> (rule5 % int4))) -> (rule4 % int3)) ((triple6 triple5) -> (rule5 % int4))) -> (rule7 % int2))) -> (rule9 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int3
Fiona is cold.
("Fiona" "is" "cold" "+")
int4
Fiona is green.
("Fiona" "is" "green" "+")
((((((((triple5 ((triple6 triple5) -> (rule5 % int5))) -> (rule4 % int4)) ((triple6 triple5) -> (rule5 % int5))) -> (rule7 % int3))) -> (rule9 % int2))) -> (rule2 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
int3
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int4
Fiona is cold.
("Fiona" "is" "cold" "+")
int5
((((((((triple5 ((triple6 triple5) -> (rule5 % int5))) -> (rule4 % int4)) ((triple6 triple5) -> (rule5 % int5))) -> (rule7 % int3))) -> (rule9 % int2))) -> (rule3 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
int3
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int4
Fiona is cold.
("Fiona" "is" "cold" "+")
int5