Dave is big. Erin is nice. Gary is white. Harry is round. All big, smart things are blue. All nice, big things are smart. If Dave is white and Dave is big then Dave is rough. Big things are nice. All rough things are nice. If Harry is nice and Harry is blue then Harry is white.
Dave is big.
("Dave" "is" "big" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Gary is white.
("Gary" "is" "white" "+")
Harry is round.
("Harry" "is" "round" "+")
All big, smart things are blue.
((("something" "is" "big" "+") ("something" "is" "smart" "+")) -> ("something" "is" "blue" "+"))
All nice, big things are smart.
((("something" "is" "nice" "+") ("something" "is" "big" "+")) -> ("something" "is" "smart" "+"))
If Dave is white and Dave is big then Dave is rough.
((("Dave" "is" "white" "+") ("Dave" "is" "big" "+")) -> ("Dave" "is" "rough" "+"))
Big things are nice.
((("something" "is" "big" "+")) -> ("something" "is" "nice" "+"))
All rough things are nice.
((("something" "is" "rough" "+")) -> ("something" "is" "nice" "+"))
If Harry is nice and Harry is blue then Harry is white.
((("Harry" "is" "nice" "+") ("Harry" "is" "blue" "+")) -> ("Harry" "is" "white" "+"))
Harry is round.
True
1
proof
[(triple4)]
("Harry" "is" "round" "+")
triple4
Dave is not big.
False
1
inv-proof
[(triple1)]
("Dave" "is" "big" "-")
triple1
Dave is nice.
True
2
proof
[(((triple1) -> rule4))]
("Dave" "is" "nice" "+")
((triple1) -> (rule4 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is not nice.
False
2
inv-proof
[(((triple1) -> rule4))]
("Dave" "is" "nice" "-")
((triple1) -> (rule4 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is smart.
True
4
proof
[(((((triple1) -> rule4) triple1) -> rule2))]
("Dave" "is" "smart" "+")
((((triple1) -> (rule4 % int2)) triple1) -> (rule2 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is not smart.
False
4
inv-proof
[(((((triple1) -> rule4) triple1) -> rule2))]
("Dave" "is" "smart" "-")
((((triple1) -> (rule4 % int2)) triple1) -> (rule2 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is blue.
True
6
proof
[(((triple1 ((((triple1) -> rule4) triple1) -> rule2)) -> rule1))]
("Dave" "is" "blue" "+")
((triple1 ((((triple1) -> (rule4 % int3)) triple1) -> (rule2 % int2))) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is not blue.
False
6
inv-proof
[(((triple1 ((((triple1) -> rule4) triple1) -> rule2)) -> rule1))]
("Dave" "is" "blue" "-")
((triple1 ((((triple1) -> (rule4 % int3)) triple1) -> (rule2 % int2))) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Harry is not blue.
Unknown
inv-rconc
[@1: Harry is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "blue" "-")
Erin is blue.
Unknown
rconc
[@1: Erin is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "blue" "+")
Dave is not rough.
Unknown
inv-rconc
[@1: Dave is rough.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "rough" "-")
Harry is nice.
Unknown
rconc
[@1: Harry is nice.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Harry" "is" "nice" "+")
Harry is not rough.
Unknown
inv-random
[@0: Harry is rough.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "rough" "-")
Harry is big.
Unknown
random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "+")
Gary is not rough.
Unknown
inv-random
[@0: Gary is rough.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "rough" "-")
Erin is rough.
Unknown
random
[@0: Erin is rough.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "rough" "+")
@0: Dave is big.[(triple1)] Erin is nice.[(triple2)] Gary is white.[(triple3)] Harry is round.[(triple4)] @1: Dave is nice.[(((triple1) -> rule4))] @2: Dave is smart.[(((((triple1) -> rule4) triple1) -> rule2))] @3: Dave is blue.[(((triple1 ((((triple1) -> rule4) triple1) -> rule2)) -> rule1))]
Dave is big.
("Dave" "is" "big" "+")
triple1
Erin is nice.
("Erin" "is" "nice" "+")
triple2
Gary is white.
("Gary" "is" "white" "+")
triple3
Harry is round.
("Harry" "is" "round" "+")
triple4
Dave is nice.
("Dave" "is" "nice" "+")
((triple1) -> (rule4 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
((((triple1) -> (rule4 % int2)) triple1) -> (rule2 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
((triple1 ((((triple1) -> (rule4 % int3)) triple1) -> (rule2 % int2))) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3