Dave is smart. Erin is smart. Fiona is smart. Harry is red. If Erin is nice then Erin is red. If someone is smart then they are nice.
Dave is smart.
("Dave" "is" "smart" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Harry is red.
("Harry" "is" "red" "+")
If Erin is nice then Erin is red.
((("Erin" "is" "nice" "+")) -> ("Erin" "is" "red" "+"))
If someone is smart then they are nice.
((("someone" "is" "smart" "+")) -> ("someone" "is" "nice" "+"))
Fiona is smart.
True
1
proof
[(triple3)]
("Fiona" "is" "smart" "+")
triple3
Fiona is not smart.
False
1
inv-proof
[(triple3)]
("Fiona" "is" "smart" "-")
triple3
Erin is nice.
True
2
proof
[(((triple2) -> rule2))]
("Erin" "is" "nice" "+")
((triple2) -> (rule2 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Dave is not nice.
False
2
inv-proof
[(((triple1) -> rule2))]
("Dave" "is" "nice" "-")
((triple1) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Erin is red.
True
3
proof
[(((((triple2) -> rule2)) -> rule1))]
("Erin" "is" "red" "+")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is not red.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule1))]
("Erin" "is" "red" "-")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Harry is not nice.
Unknown
inv-rconc
[@1: Harry is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "nice" "-")
Fiona is cold.
Unknown
random
[@0: Fiona is cold.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "cold" "+")
Erin is not big.
Unknown
inv-random
[@0: Erin is big.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "big" "-")
Fiona is big.
Unknown
random
[@0: Fiona is big.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "big" "+")
Dave is not red.
Unknown
inv-random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "-")
Erin is cold.
Unknown
random
[@0: Erin is cold.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "cold" "+")
@0: Dave is smart.[(triple1)] Erin is smart.[(triple2)] Fiona is smart.[(triple3)] Harry is red.[(triple4)] @1: Dave is nice.[(((triple1) -> rule2))] Erin is nice.[(((triple2) -> rule2))] Fiona is nice.[(((triple3) -> rule2))] @2: Erin is red.[(((((triple2) -> rule2)) -> rule1))]
Dave is smart.
("Dave" "is" "smart" "+")
triple1
Erin is smart.
("Erin" "is" "smart" "+")
triple2
Fiona is smart.
("Fiona" "is" "smart" "+")
triple3
Harry is red.
("Harry" "is" "red" "+")
triple4
Dave is nice.
("Dave" "is" "nice" "+")
((triple1) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
((triple2) -> (rule2 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
((triple3) -> (rule2 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2