Dave is cold. Dave is nice. Dave is quiet. Erin is big. Erin is blue. Erin is quiet. Erin is smart. Gary is big. Gary is quiet. Gary is smart. Harry is blue. Harry is nice. Harry is quiet. Harry is red. Harry is smart. All cold things are quiet. Nice, blue things are red. If something is smart then it is quiet. If something is cold and red then it is smart. All smart things are big. Big things are smart.
Dave is cold.
("Dave" "is" "cold" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is smart.
("Harry" "is" "smart" "+")
All cold things are quiet.
((("something" "is" "cold" "+")) -> ("something" "is" "quiet" "+"))
Nice, blue things are red.
((("something" "is" "nice" "+") ("something" "is" "blue" "+")) -> ("something" "is" "red" "+"))
If something is smart then it is quiet.
((("something" "is" "smart" "+")) -> ("something" "is" "quiet" "+"))
If something is cold and red then it is smart.
((("something" "is" "cold" "+") ("something" "is" "red" "+")) -> ("something" "is" "smart" "+"))
All smart things are big.
((("something" "is" "smart" "+")) -> ("something" "is" "big" "+"))
Big things are smart.
((("something" "is" "big" "+")) -> ("something" "is" "smart" "+"))
Harry is blue.
True
1
proof
[(triple11)]
("Harry" "is" "blue" "+")
triple11
Erin is not big.
False
1
inv-proof
[(triple4 OR ((triple7) -> rule5))]
("Erin" "is" "big" "-")
triple4
((triple7) -> (rule5 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is not red.
Unknown
inv-rconc
[@1: Erin is red.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Erin" "is" "red" "-")
Gary is blue.
Unknown
random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "+")
@0: Dave is cold.[(triple1)] Dave is nice.[(triple2)] Dave is quiet.[(triple3 OR ((triple1) -> rule1))] Erin is big.[(triple4 OR ((triple7) -> rule5))] Erin is blue.[(triple5)] Erin is quiet.[(triple6 OR ((triple7) -> rule3) OR ((((triple4) -> rule6)) -> rule3))] Erin is smart.[(triple7 OR ((triple4) -> rule6))] Gary is big.[(triple8 OR ((triple10) -> rule5))] Gary is quiet.[(triple9 OR ((triple10) -> rule3) OR ((((triple8) -> rule6)) -> rule3))] Gary is smart.[(triple10 OR ((triple8) -> rule6))] Harry is blue.[(triple11)] Harry is nice.[(triple12)] Harry is quiet.[(triple13 OR ((triple15) -> rule3))] Harry is red.[(triple14 OR ((triple12 triple11) -> rule2))] Harry is smart.[(triple15)] @1: Harry is big.[(((triple15) -> rule5))]
Dave is cold.
("Dave" "is" "cold" "+")
triple1
Dave is nice.
("Dave" "is" "nice" "+")
triple2
Dave is quiet.
("Dave" "is" "quiet" "+")
triple3
((triple1) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
triple4
((triple7) -> (rule5 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
triple5
Erin is quiet.
("Erin" "is" "quiet" "+")
triple6
((triple7) -> (rule3 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
((((triple4) -> (rule6 % int2))) -> (rule3 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
triple7
((triple4) -> (rule6 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
triple8
((triple10) -> (rule5 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
triple9
((triple10) -> (rule3 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
((((triple8) -> (rule6 % int2))) -> (rule3 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
triple10
((triple8) -> (rule6 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
triple11
Harry is nice.
("Harry" "is" "nice" "+")
triple12
Harry is quiet.
("Harry" "is" "quiet" "+")
triple13
((triple15) -> (rule3 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
triple14
((triple12 triple11) -> (rule2 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
triple15
Harry is big.
("Harry" "is" "big" "+")
((triple15) -> (rule5 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1